T:Type, P:(T), L:(T List), x:T. (x  filter(P; L))  ((x  L)  ((P(x)))) 

latex

Definitions	t  T, Y, reduce(f; k; as), filter(P; l), x:A. B(x), x. t(x), P  Q, P  Q, P  Q, P  Q, prop{i:l}, ff, tt, if b then t else f fi , P  Q, guard(T), True, x(s), False, Unit, , A,
Lemmas	bool wf, and functionality wrt iff, nil member, iff functionality wrt iff, all functionality wrt iff, false wf, assert wf, l member wf, iff wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, not wf, bnot wf, cons member, filter wf